{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# LTL Synthesis Hierarchical Transformer Experiment"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Imports"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import tensorflow as tf\n",
    "\n",
    "from ml2.ltl import LTLSpec\n",
    "from ml2.ltl.ltl_syn.ltl_syn_hier_transformer_experiment import LTLSynHierTransformerExperiment"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Create Experiment"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "experiment = LTLSynHierTransformerExperiment()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Run Experiment"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "experiment.run(stream_to_wandb=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Load Experiment"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "INFO:ml2.artifact:Found experiment hier-transformer-0 locally\n",
      "INFO:ml2.experiment:Initialized experiment with arguments:\n",
      "aiger_order: ['inputs', 'latches', 'outputs', 'ands']\n",
      "aiger_unfold_latches: False\n",
      "aiger_unfold_negations: False\n",
      "alpha: 1.0\n",
      "batch_size: 256\n",
      "beam_size: 1\n",
      "cache_dataset: True\n",
      "checkpoint_monitor: val_accuracy_per_sequence\n",
      "constant_learning_rate: None\n",
      "custom_pos_enc: True\n",
      "d_embed_dec: 256\n",
      "d_embed_enc: 256\n",
      "d_ff_dec: 1024\n",
      "d_ff_enc_d0: 1024\n",
      "d_ff_enc_d1: 1024\n",
      "dataset_name: scpa-2\n",
      "drop_batch_remainder: True\n",
      "dropout_dec: 0.0\n",
      "dropout_enc: 0.0\n",
      "dtype_float: <dtype: 'float32'>\n",
      "dtype_int: <dtype: 'int32'>\n",
      "encode_realizable: True\n",
      "ff_activation_dec: relu\n",
      "ff_activation_enc_d0: relu\n",
      "ff_activation_enc_d1: relu\n",
      "group: None\n",
      "initial_steps: 0\n",
      "inputs: ['i0', 'i1', 'i2', 'i3', 'i4']\n",
      "max_input_length: 128\n",
      "max_target_length: 128\n",
      "name: hier-transformer-0\n",
      "num_heads_dec: 4\n",
      "num_heads_enc_d0: 4\n",
      "num_heads_enc_d1: 4\n",
      "num_layers_dec: 8\n",
      "num_layers_enc_d0: 4\n",
      "num_layers_enc_d1: 4\n",
      "num_properties: 12\n",
      "outputs: ['o0', 'o1', 'o2', 'o3', 'o4']\n",
      "parent_name: \n",
      "property_tree_size: 25\n",
      "shuffle_on_load: False\n",
      "steps: 30000\n",
      "tf_shuffle_buffer_size: 0\n",
      "val_freq: 100\n",
      "warmup_steps: 4000\n",
      "WARNING:ml2.experiment:Experiment hier-transformer-0 already exists locally\n"
     ]
    }
   ],
   "source": [
    "experiment = LTLSynHierTransformerExperiment.load('hier-transformer-0')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "tags": []
   },
   "source": [
    "## Evaluate Test Set"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "experiment.batch_size = 16\n",
    "experiment.beam_size = 16\n",
    "experiment.alpha = 0.5"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "experiment.eval('test', steps=8, training=False, verify=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Evaluate SYNTCOMP"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "experiment.eval_ltl_specs('sc-0')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Evaluate Timeouts"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "experiment.eval_timeouts(steps=8, training=False)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Evaluate Smart Home Benchmarks"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "experiment.eval_bosy_files('syntcomp/tsl_smart_home_jarvis')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Analyze Evaluations"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "EVAL_DIR = ''\n",
    "experiment.analyze_eval_circuits(\n",
    "    EVAL_DIR,\n",
    "    buckets=[5, 10, 15, 20],\n",
    "    property='Num AND Gates',\n",
    "    title='Test Set',\n",
    "    width=3.0,\n",
    "    xlabel='Number of AND Gates')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "FILEPATH = ''\n",
    "experiment.analyze_eval_file_realizability(FILEPATH)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Call Model"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "spec_dict = {\n",
    "    \"guarantees\": [\n",
    "        \"G (! o0 | ! o1)\",\n",
    "        \"(G ((i0) -> (F (o0))))\",\n",
    "        \"(G ((i1) -> (F (o1))))\"\n",
    "      ],\n",
    "      \"inputs\": [\n",
    "        \"i0\",\n",
    "        \"i1\",\n",
    "        \"i2\",\n",
    "        \"i3\",\n",
    "        \"i4\"\n",
    "      ],\n",
    "      \"outputs\": [\n",
    "        \"o0\",\n",
    "        \"o1\",\n",
    "        \"o2\",\n",
    "        \"o3\",\n",
    "        \"o4\"\n",
    "      ],\n",
    "}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "problem = LTLSpec.from_dict(spec_dict)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "experiment.call(problem, training=False, verify=True)"
   ]
  }
 ],
 "metadata": {
  "interpreter": {
   "hash": "8caa4319d59a734f94e739df6b594acde678ec5f2e3eb7152d087fc4a1992669"
  },
  "kernelspec": {
   "display_name": "Python 3.7.3 64-bit ('ml2': pyenv)",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.3"
  },
  "metadata": {
   "interpreter": {
    "hash": "6777b983a30343457facb6d641fab749a3d1ac686971770ba4e1636635b77c7f"
   }
  },
  "orig_nbformat": 2
 },
 "nbformat": 4,
 "nbformat_minor": 2
}
